%\paragraph{Motivation}
Process calculi aim at describing formally the behavior of concurrent systems. 
A leading motivation in the development of process calculi has been 
properly capturing the \emph{dynamic character} of concurrent behavior.
In fact, much of the success of the $\pi$-calculus~\cite{MilnerPW92a} can be fairly attributed to 
the way it departs from CCS~\cite{Milner89} so as to describe 
mobile systems in which  communication topologies can change dynamically.
Subsequent developments can be explained similarly. 
For instance, the Ambient calculus~\cite{CardelliG00} 
builds on $\pi$-calculus mobility 
to describe the dynamics of interaction within 
boundaries and hierarchies, as
required in distributed systems.
%complements mobility as in the $\pi$-calculus with the 
%dynamics of interaction within 
%with boundaries and hierarchies, thus capturing issues of space/context awareness 
%For instance, 
%the introduction of the Ambient calculus~\cite{CardelliG00} %(and related formalisms) 
%can be justified by the need of describing mobility with considerations of , 
%common in distributed systems.
A commonality in these calculi is that 
the dynamic behavior of a system is realized through a number of \emph{local changes}, 
usually formalized by reduction steps.
Indeed, while in the $\pi$-calculus mobility is enforced by the reconfiguration of individual linkages in the communication topology, % is what characterizes mobility,
in the Ambient calculus spatial mobility is obtained by individual modifications to the containment relations within the ambient hierarchy.
This way, the combined effect of a series of changes at a local level (links, containment relations) 
suffices to explain dynamic behavior at the global (system) level.


%Crucially, in both these formalisms 
%the dynamic behavior of a system is realized through a number of \emph{local changes}, 
%formalized by reduction steps:
%% in its topology:
%while in the $\pi$-calculus the reconfiguration of a single linkage in the communication topology characterizes mobility, 
%in the Ambient calculus  spatial mobility arises from the modification to a single containment relation in the hierarchy of ambients.
%%In both cases, changes at a local level are conceptually lifted to explain concurrent behavior at the global (system) level.
%%This way, the combined effect of local changes suffices to explain dynamic behavior at the global (system) level.
%Consequently, 
%dynamic behavior at the global (system) level can only be obtained 
%from the combined effect of a series of changes at the local level.

There are, however, interesting forms of dynamic behavior that cannot be satisfactorily 
described as a combination of local changes, in the above sense.
These are behavioral patterns which concern change at the \emph{process} level (i.e., the process as a whole), 
and describe \emph{process evolution} along time.
In general, forms of process evolvability are 
characterized by an enhanced control/awareness over 
the current behavior and location of running processes. 
Crucially, this increased control is central to the 
\emph{adaptation} capabilities by which processes modify 
their behavior in response to exceptional 
circumstances in their environment.
As a simple example, 
consider  a scheduler in an operating system which 
% executes, suspends, and resumes 
manages the execution of 
a  set of processes.
To specify the behavior of the scheduler, the processes, and their evolution, 
we would need mechanisms for \emph{direct} process manipulation, 
which appear hard  to represent 
in calculi enforcing 
%by means of 
%link mobility 
local changes only. 
More precisely, 
it is not clear at all how to represent 
the \emph{intermittent evolution} of a process under the scheduler's control: that is, precise ways of describing that 
its behavior 
``disappears'' (when the scheduler suspends the process)
and
``appears'' (when the scheduler resumes the process). 
Emerging applications and programming paradigms 
provide challenging examples of
evolvable processes. % and their associated challenges.
In workflow applications, we would like to be able to replace  a running activity, 
%without affecting the rest of the workflow.
%We might also like to 
suspend the execution of a set of activities, or even suspend and relocate the whole workflow.
Similarly, in component-based systems we would like to
reconfigure parts of a component, a whole component, or groups of components.
Also, 
we would like to specify the 
context-aware policies that dynamically adapt the
computational power 
of cloud computing 
applications.
% at runtime.
%scaling policies that 
%reconfigure the
%remove and add instances of 
%computational power at runtime.
%These are 
%to the user's demand. % and are highly dynamic.
%(We elaborate on these examples in Section~\ref{s:examp}.)
At the heart of these applications we find 
forms of process evolution and adaptation which appear very difficult (if not impossible) to express
in existing process calculi. 

\paragraph{A Core Calculus of Adaptable Processes}
In an attempt to address these shortcomings, this paper introduces the concept of \emph{adaptable processes}. 
Adaptable processes have a location and 
are sensible to actions of \emph{dynamic update} at runtime.
While locations are useful to designate and structure processes into hierarchies,
dynamic update actions 
%allow to implement forms of process evolvability.
implement a sort of built-in adaptation mechanism.
We illustrate this novel concept by 
 introducing \evol{}, a core process calculus of adaptable processes. % (Section \ref{s:calculi}).
The \evol{} calculus arises as
 a variant of CCS without restriction and relabeling, and 
extended with primitive notions of location and dynamic update.
In $\mathcal{E}$,  
$\component{a}{P}$ denotes the adaptable process $P$ located at $a$.
Name $a$ acts as a \emph{transparent locality}: $P$ can 
evolve on its own but also  
interact freely with its environment.
Localities can be nested, and are sensible to interactions with \emph{update prefixes}.
An update prefix $\update{a}{U}$ decrees the update of the adaptable process at $a$
with the behavior defined by 
%\emph{update patterns}
$U$, a \emph{context} with zero or more holes,  denoted by $\bullet$.
The \emph{evolution} of $\component{a}{P}$  is realized by 
its interaction  
with the update prefix 
$\update{a}{U}$, which leads to 
%process 
%$U \sub P \bullet$, 
%, which represents 
%$U[P]$, 
%i.e., 
the process obtained by replacing every hole $\bullet$ in $U$ by $P$, denoted 
\fillcon{U}{P}.



%We investigate the decidability of 
%%bounded and eventual adaptation 
%\OG and \LG 
%in 
We consider several variants of \evol{},  obtained via  
two orthogonal characterizations.
%The properties of Evolvable CCS depend on its syntax and on restrictions on such a syntax. 
%\begin{list}{\labelitemii}{\leftmargin=1em}
%\item 
The first one is 
\emph{structural}, and % characterization
%distinguishes between
defines 
\emph{static} and \emph{dynamic} topologies of adaptable processes.
In a static topology, the number of adaptable processes does not vary along the evolution of the system:
they cannot be destroyed nor new ones can appear. %, by e.g. putting them after a prefix.
%Hence, for example, in a static topology, any $\update{a}{U}$ is required to be such that $U = \component{a}{U'}$, thus
%any interaction of $\component{a}{P}$ with $\update{a}{U}$
%leads necessarily to component $\component{a}{U \sub P \bullet}$. 
In contrast, in the more general dynamic topology this restriction is lifted. 
We will use the subscripts $s$ and $d$ to denote the 
variants of \evol{} with static and dynamic topologies,
respectively.
The second characterization is 
%\item A 
\emph{behavioral}, and  %characterization  
concerns 
%features of  of 
\emph{update patterns}---the 
context 
$U$ in an update prefix $\update{a}{U}$.
As hinted at above, update patterns determine the 
 behavior of running processes after an update action.
In order to account for different evolvability patterns, 
we consider three kinds of update patterns, which determine three 
families of \evol{} calculi---denoted by the superscripts 
1, 2, and 3, respectively.
%\evol{1}, \evol{2}, and \evol{3}, respectively.
%\footnote{The family \evol{2} has been called \evol{-} in abridged versions of the present work (\cite{BGPZFMOODS}).}
The first update pattern 
admits all kinds of contexts, and so it represents  
the most expressive form of update. 
In particular, holes $\bullet$ can appear behind prefixes.
The second update pattern forbids such guarded holes in contexts. 
In the third update pattern we further require contexts to have exactly one hole, 
thus preserving the current behavior (and possibly adding new behaviors): 
this is the most restrictive form of update. 
%\end{list}

%\begin{example}
%\input{example}\qed
%\end{example}

%\todo{motivation for the static/dynamic distinction??}
In our view, 
%the variants of  \evol{}  derived from these two characterizations 
these variants
capture a fairly ample spectrum of scenarios that arise in the 
joint
analysis of correctness and adaptation concerns in evolvable systems.
%component aggregations.
They borrow inspiration from 
existing programming languages,
development frameworks, and 
component models.
%Our structural characterization 
%%can be seen as an attempt to  
%aims at 
%capturing %and generalize the 
%the distinctions between ``flat'' component models (such as, e.g., EJB~\cite{ejb} and CCM~\cite{ccm}) and
%``hierarchical'' ones (such as, e.g., Fractal~\cite{fractal}, SOFA 2~\cite{sofa}).
The structural characterization follows the premise that 
while it is appealing to define the runtime evolution of
 the structures underlying 
aggregations of behaviors, in some scenarios 
it is also sensible to specify evolution and adaptation preserving such structures.
For instance, 
we would like software updates to preserve the main architecture of our operating system; 
conversely, an operating system could be designed to disallow runtime updates that alter its basic organization in dangerous ways.  
A static topology is also consistent with settings in which 
adaptable processes represent \emph{located resources}, 
whose creation 
is disallowed or 
comes with a cost (as in cloud computing scenarios).
The behavioral characterization
%our update patterns 
is inspired in the  
(restricted) forms 
of reconfiguration and/or update  available in component models 
in which evolvability is specified in terms of 
%suitable behavioral 
patterns, such as SOFA 2~\cite{HnetynkaP06}.
Update patterns are also related to functionalities present in 
programming languages such as Erlang~\cite{erlang,Armstrong03} and in
development frameworks such as the Windows Workflow Foundation (WWF)~\cite{wwf}.
%and component models such as Fractal \cite{fractal}.
In fact, 
forms of dynamic update behavior for workflow services in the WWF
include the possibility of replacing and removing service contracts 
(analogous to our first and second update patterns)
and also the addition of new service contracts and operations 
(as in our third update pattern, which preserves existing behavior and operations).
%Our framework can also be related to 
%mechanisms for software update/upgrade in 
%operating systems such as Windows Update and Linux distributions.

\paragraph{Verification of Adaptable Processes}
Rather than a specification language, the \evol{} calculus intends to be a basis for 
investigating the fundamental properties of evolvable processes.
%and for developing richer languages with evolvability capabilities.
In this presentation, we study  two  \emph{verification problems} associated to $\mathcal{E}$ processes and their (un)decidability.
%We propose two such problems. 
%correctness properties for $\mathcal{E}$ processes.
They are defined in terms of standard observability predicates (\emph{barbs}), which indicate the presence of a designated error signal.
We thus distinguish between \emph{correct states} (i.e., states in which no error barbs are observable) and \emph{error states} (i.e., states exhibiting error barbs).
The first verification problem, 
\emph{bounded adaptation} 
(abbreviated \OG)
ensures that,
given a finite $k$, 
at most $k$ consecutive error states can arise  in computations of the system---including those reachable as a result of
dynamic updates.
The second one, 
\emph{eventual adaptation} (abbreviated \LG), 
is similar but weaker: 
it ensures that if the system enters into an error state then it will eventually reach a correct 
state. %---that is,  it ensures that only finitely many errors can occur.
We believe that 
\OG and \LG
%bounded and eventual adaptation 
fit well in 
the kind of correctness analysis that is required in a number of emerging applications.  
%including, but not limiting to, cloud computing scenarios.
%Returning to the cloud computing setting motivated at the beginning, 
%these properties allow to check, 
For instance, 
on the provider side of a cloud computing application, %it is possible to check 
these properties allow to check
whether a 
client is able to assemble faulty systems
via the aggregation of the provided services and the possible subsequent updates.
On the client side, it is possible to 
%perform forms of 
carry out forms of 
\emph{traceability analysis}, so as to 
prove that if 
%an incorrect computation has been executed by the system, 
the system exhibits an incorrect behavior, then 
it follows from a bug in the provider's infrastructure
and not from the initial aggregation and dynamic updates 
provided by the client.


In addition to  
error occurrence, 
%to characterize forms of error, 
the correctness of
adaptable processes 
must consider the fact 
%it is fundamental to take into account 
that the number of 
modifications (i.e. update actions)
that can be 
applied to the system is typically \emph{unknown}. 
For this reason, we 
consider \OG and \LG in conjunction with 
the notion of \emph{cluster} of adaptable processes.
Given a system $P$ and a set $M$ of possible updates that
can be applied to it at runtime, 
its associated cluster considers $P$ together 
with an arbitrary number of instances of the updates in $M$.
%that can be performed over $P$ at runtime.
This way, 
a cluster  formalizes adaptation and correctness properties 
of an initial system configuration (represented by an aggregation of adaptable processes)
in the presence of arbitrarily many sources of update actions.
For instance, in a cloud computing scenario %sketched earlier:
the notion of cluster captures 
the cloud application as initially deployed by the client along with 
the options offered by the provider for 
its evolution at runtime. 

%we propose three
%different \emph{aggregation schemas}, 
%which are taken into consideration 
%when investigating the (un)decidability of \OG and \LG.
%The first schema, called \emph{standalone aggregation},
%%is the most elementary form of aggregation and 
%concerns the correctness of a single component in isolation.
%The second aggregation schema, called \emph{parallel aggregation},
%%concerns the correctness of a set of  
%represents 
%components which can be combined only under parallel contexts.
%This schema is subsumed by \emph{updatable aggregation}, 
%in which the set of components can be combined 
%under contexts containing parallel composition but also using transparent localities.
%Hence, updatable aggregations subsume parallel aggregations, which in turn subsume standalone aggregation. 
%We believe that these aggregation schemas provide 
%an incremental, fine-grained approach to assess the
%influence of external contexts on the correctness of a set of components.

%\newpage

%A comment on our notion of component is worthwhile. 
%As mentioned earlier, we use the term \emph{component} in a very broad sense. 
%Component models  typically consider stateful entities with 
%\emph{interfaces}, 
%which specify conditions for composition and/or behavioral compatibility.
%We have chosen to formalize components by abstracting from the notion of interface (and its associated issues,  
%e.g., interface mismatches), and have relied on transparent localities for describing containment/hierarchy.
%The reasons for this choice are twofold. On the one hand, we are interested in 
%correctness and adaptation 
%in dynamic reconfiguration
%from a general perspective, and so including particular notions of interface would have limited the generality of our results. 
%%In fact, as mentioned before, motivations for our study arise from component models but also from other emerging applications 
%%such as cloud computing and workflow management 
%%in which component-like notions  are present. 
%%An immediate advantage of 
%By abstracting from interfaces in this way our  results shed 
%light on the nature of bounded and eventual adaptation in areas including---but not limiting to---component-based systems.
%%in areas in which notions similar to component  are present. 
%On the other hand, the analysis of  adaptation becomes substantially harder
%when considering interfaces.
%In fact, we conjecture undecidability of \OG and \LG for the six variants of \evol{}, even with very simple interfaces.
%In our view, rather than investigating (un)decidability issues in a fully-fledged formalism with interfaces, 
%a more reasonable research strategy is to identify first the variants of \evol{} in which adaptation is decidable---thus spotting where decidability lies---, 
%and then to investigate the actual influence interfaces have in expressiveness and (un)decidability results.


%\end{list}

\paragraph{Contributions}
The main technical results of the paper are summarized in Table \ref{t:results}.
The calculus \evol{1} is shown to be Turing complete, 
%thus evidencing the expressive power of update actions.
%As a result, 
and both \OG and \LG are shown to be 
\emph{undecidable} for \evol{1} processes. % (Section~\ref{s:ev1}).
The Turing completeness of \evol{1} says much on the expressive power of update actions.
In fact, it is known that fragments of CCS without restriction
can be translated into finite Petri nets (see, e.g.,  the discussion in \cite{Bravetti09}), and so they are not Turing complete.
Update actions in \evol{} thus allow to ``jump''  from finite Petri nets to a Turing complete model.
We then show that in \evol{2} 
\OG is \emph{decidable}, % (Section~\ref{sec:decwsts}), 
while \LG remains \emph{undecidable}. % (Section~\ref{sec:unde2d}).
Interestingly,  \LG is already undecidable in \evold{3}, while it is \emph{decidable} in \evols{3}. 
 

\begin{table}[t]
%\begin{figure}[t]
%\begin{floatingtable}[r]{
\begin{center}
\begin{tabular}{c|c|c}
		& \evold{} -- Dynamic Topology & \evols{} -- Static Topology \\
\hline \hline
\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
\hline
\evol{2}	& ~ \OG dec~/~\LG undec ~ & ~ \OG dec~/~\LG undec \\
\hline
\evol{3}	& ~ \OG dec~/~\LG undec ~ & \OG~dec~/~\LG dec 
\end{tabular}
\end{center}
\caption{\label{t:results} Summary of  (un)decidability results for dialects of \evol{}.}
%We use \evol{i} to denote the family of \evol{} with the $i$-th update pattern.
%\end{figure}
%\end{floatingtable}
 \linefigure
\end{table}



%\noindent
%The table at the right 
We now comment on the proof techniques.
The decidability of 
\LG in \evols{3} 
is proved by resorting to 
Petri nets: %. More precisely, 
\LG is reduced to a problem on Petri nets that we call \emph{infinite visits} which, in turn, can 
be reduced to \emph{place boundedness}---a decidable problem  for Petri nets. 
For the decidability of 
\OG we appeal to the theory of 
\emph{well-structured transition systems}  \cite{FinkelS01,AbdullaCJT00}
and its associated results. 
%For \evol{1} and \evol{2},
%we identify and formalize a relationship between static and dynamic topologies that allows us to
%transfer (un)decidability results in both directions.
In our case,  such a theory %of well-structured transition systems 
must be coupled with Kruskal's theorem \cite{kruskal60} 
(which allows to deal with terms whose syntactical tree structure has an unbounded depth), and
with the calculation of the predecessors of target terms in the context of trees with unbounded depth 
(which is necessary in
order to deal with arbitrary aggregations
and dynamic updates that may generate new adaptable processes). 
This combination of techniques %and results 
proved to be very challenging.
In particular, 
the technique is more complex than that in \cite{AB09}, which relies on a bound on the depth of trees, or that 
in \cite{WZH10}, where only topologies with bounded paths are taken into account.
Kruskal's theorem is also used in \cite{Bravetti09} for studying the decidability properties of calculi with 
exceptions and compensations. The calculi considered in \cite{Bravetti09}
are \emph{first-order}; in contrast, 
%because of the term instantiation mechanism associated to component update, 
%as elaborated  in \cite{BGPZFACS}, 
\evol{} can be considered as a \emph{higher-order} calculus (see Section~\ref{s:rw}).

The undecidability results are obtained via encodings of Minsky machines \cite{Minsky67}, 
a well-known Turing complete model. 
In particular, the encodings that we provide 
for showing undecidability of  \LG in \evol{2} and \evold{3} 
do not reproduce 
faithfully the corresponding machine, but only finitely many steps
are wrongly simulated. 
Similar techniques have been used to prove the undecidability
of repeated coverability in reset Petri nets~\cite{E03}, 
but in our case
their application revealed much more complex;
this is particularly true for the case of \evold{3} 
%(i.e., the family of \evol{} with the third update pattern),
where there is 
no native mechanism for \emph{removing} an arbitrary amount of processes.  
Moreover, as in a cluster there is no a-priori knowledge of the 
number of modifications that will be applied to the system, we need
to perform a parametric analysis. Parametric verification has been
studied, e.g., in the context of broadcast protocols
in both fully connected~\cite{EsparzaFM99} and ad-hoc 
networks~\cite{DelzannoSZ10}.
 Differently from \cite{EsparzaFM99,DelzannoSZ10}, 
% the  parametrized verification presented in those works, 
in which 
the number of nodes (or the topology) of the network 
is unknown,
we consider systems in which there is a known part  (the initial
system $P$), and there is another part composed of an unknown
number of process instances  (taken from 
$M$, the set of possible modifications). \\

\noindent Summing up, in the present paper we make the following contributions:
%\begin{list}{\labelitemii}{\leftmargin=1em}
\begin{enumerate}

\item We introduce $\evol{}$, a core calculus of adaptable processes.
\evol{} allows to express a wide range of patterns of process evolution and runtime adaptation.
By means of structural and behavioral characterizations, we 
identify different meaningful variants of the language.  
We are not aware of other process calculi 
tailored to the joint representation of 
evolution and adaptation concerns 
in concurrent systems.

\item 
We introduce bounded and eventual adaptation---two correctness properties for adaptable processes---and study their (un)decidability %of these two properties 
in each of the  variants of \evol{}.
We do so by considering systems as part of clusters which define their evolvability along time.
To the best of our knowledge, ours is the first study of the (un)decidability of 
adaptation properties for dynamically evolvable processes.

\end{enumerate}



%These are fundamental issues for concurrent languages at large; 


% It is worth pointing that 
% openness is closely related to mobility and network-awareness 
% in that not only complete components might move across the predefined structure of the system, 
% but also it might occur that such a structure is reconfigured as a result of the interactions of mobile components.
% This is the case of, for instance, a running component which disconnects from one location and
% later on reconnects to some other location. 



% Some ideas:
% 
% Suspension/update in global and open systems
% 
% Suspension and evolvability patterns in component-based systems
% 
% A basic calculus for components and its sucessive enhancements (update and "hot" update).
% 
% It makes a lot of sense to study expressiveness of passivation with respect to termination properties.
% 
% 
% Two enhancements that lead to weakly Turing completeness and Turing completeness.
% 
% How robust are the results? Adding recursion and full higher-order communication
%\todo{Perhaps moving Rel Work to the end, in the concl remarks?}
%\input{relatedwork}


This paper is an extended and revised version of the conference paper~\cite{BGPZFMOODS}. 
In addition to provide full details of the technical results, 
this presentation 
thoroughly develops the structural and behavioral characterizations of adaptable processes.
This way, we present a unified treatment of the 
 distinction between the static and dynamic topologies of adaptable processes, as well as of the three different update patterns.
These ideas were treated only partially  in~\cite{BGPZFMOODS}, 
where the family \evol{2} was called \evol{-}.
In particular, new results not presented in~\cite{BGPZFMOODS}  include 
the relationship between static and dynamic topologies (Section~\ref{ss:stdyn}) and 
the decidability of \LG in \evols{3} by resorting to Petri nets (Section~\ref{sec:petri}).
Moreover, several illustrative examples and extended discussions are included.  
The content of Section~\ref{ss:facs} is based on the short paper~\cite{BGPZFACS}.

\paragraph{Structure of the document}
The rest of this paper is structured as follows.
The \evol{} calculus, its different variants, and several associated results  are presented in Section~\ref{s:calculi}. 
The two verification problems are defined in Section~\ref{s:prop}.
Section~\ref{s:examp} presents extended examples of modeling in \evol{}, in several emerging applications.
Section~\ref{s:prelim} collects basic definitions and results on Minsky machines, well-structured transition systems, and Petri nets.
(Un)decidability results for \evol{1}, \evol{2}, and \evol{3} are detailed in Sections \ref{s:ev1}, \ref{s:ev2}, and \ref{s:ev3}, respectively.
Section~\ref{s:rw} presents some additional discussions, and reviews some related works.
Section~\ref{s:conc} concludes. While proofs of the main results are included in the main text, technical details for some other results 
 (most notably, correctness proofs for the encodings) 
 are collected in the Appendix.


